Horațiu Cheval
Research Center for Logic, Optimization and Security,
Department of Computer Science,
Faculty of Mathematics and Computer Science,
University of Bucharest
Associated Researcher, Institute for Logic and Data Science
horatiu.cheval@unibuc.ro
About
I completed my PhD in 2024 in the field of proof mining, supervised by Laurențiu Leuștean. I am also interested in type theory and interactive theorem proving, the language I know best being Lean. I am currently a lecturer at the University of Bucharest.
Publications
- A matching logic theory of multi-hole contexts (with Xiaohong Chen, Dorel Lucanu and Grigore Roșu), Journal of Logical and Algebraic Methods in Programming (2026)
- 𝕂 definitions as Matching Logic theories, formally (with Xiaohong Chen, Dorel Lucanu and Grigore Roșu), FoSSaCS 2026
- Linear rates of asymptotic regularity for Halpern-type iterations (with Laurențiu Leuștean), Mathematics of Computation (2025)
- Rates of asymptotic regularity of the Tikhonov-Mann iteration for families of mappings, Revue Roumaine de Mathématiques Pures et Appliquées (2024)
- Formal Definitions and Proofs for Partial (Co)Recursive Functions (with David Nowak and Vlad Rusu), Journal of Logical and Algebraic Methods in Programming (2024)
- On modified Halpern and Tikhonov-Mann iterations (with Ulrich Kohlenbach and Laurențiu Leuștean), Journal of Optimization Theory and Applications (2023)
- Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration (with Laurențiu Leuștean), Optimization Methods and Software (2022)
Preprints
- Quantitative metastability of the Tikhonov-Mann iteration for countable families of mappings, arXiv:2406.03429 [math.OC] (2024)
Software
- Lean formalization of Applicative Matching Logic (with Bogdan Macovei)
- Lean HOAS implementation of the Dialectica interpretation and logical metatheorems based on it
- Lean formalization of results in H. Cheval and L. Leuștean. Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration, Optimization Methods and Software, 2022
- Python implementation of various fixed point iterations in W-hyperbolic spaces